\begin{zed}
  [CONTEXT, TASK, CORE]
\end{zed}

\begin{axdef}
  bare\_context: CONTEXT\\
  idles: \finset  TASK\\
  cores: \finset  CORE
\where
  \# cores = \# idles
\end{axdef}

\begin{zproof}[unnamed\$n3\$domainCheck]
prove;
\end{zproof}

\begin{zed}
STATE ::= nonexistent | ready | blocked | suspended | running
\end{zed}

%\begin{zed} %uncomment this when animate with ProZ
%\begin[disabled]{zed} %uncomment this when prove with Z/Eves
transition == (\{blocked\} \cross  \{nonexistent, ready, running, suspended\}) \cup  (\{nonexistent\} \cross  \{ready, running\}) \cup  (\{ready\} \cross  \{nonexistent, running, suspended\}) \cup  (\{running\} \cross  \{blocked, nonexistent, ready, suspended\}) \cup  (\{suspended\} \cross  \{nonexistent, ready, running\})
\end{zed}

\begin{schema}{TaskData}
  tasks: \finset  TASK\\
  running\_tasks: cores \inj  TASK\\
  executable: TASK \psurj  cores
\where
  \ran  running\_tasks \subseteq  tasks\\
  idles \subseteq  tasks\\
  \dom  executable = tasks\\
  \forall  t: \ran  running\_tasks @ running\_tasks \inv  t = executable(t)
\end{schema}

\begin{zproof}[TaskData\$domainCheck]
prove;
\end{zproof}

\begin{schema}{Init\_TaskData}
  TaskData'
\where
  tasks' = idles
\end{schema}

\begin{theorem}{TaskDataInit}
\forall  r: cores \inj  TASK; e: TASK \psurj  cores | r \neq  \emptyset \land  r = cores \cross  idles \land  e = r \inv  @ \exists  TaskData' @ Init\_TaskData
\end{theorem}

\begin{zproof}[TaskDataInit]
instantiate running\_tasks' == r, executable' == e;
prove by reduce;
\end{zproof}

\begin{schema}{StateData}
  state: TASK \fun  STATE
\where
  \forall  i: idles @ state(i) \in  \{ready, running\}
\end{schema}

\begin{schema}{Init\_StateData}
  StateData'
\where
  state' = (\lambda  x: TASK @ nonexistent) \oplus  (idles \cross  \{running\})
\end{schema}

\begin{theorem}{StateDataInit}
\exists  StateData' @ Init\_StateData
\end{theorem}

\begin{zproof}[StateDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{ContextData}
  phys\_context: cores \fun  CONTEXT\\
  log\_context: TASK \fun  CONTEXT
\end{schema}

\begin{schema}{Init\_ContextData}
  ContextData'
\where
  phys\_context' = (\lambda  c: cores @ bare\_context)\\
  log\_context' = (\lambda  x: TASK @ bare\_context)
\end{schema}

\begin{theorem}{ContextDataInit}
\exists  ContextData' @ Init\_ContextData
\end{theorem}

\begin{zproof}[ContextDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{PrioData}
  priority: TASK \fun  \nat 
\where
  \forall  i: idles @ priority(i) = 0
\end{schema}

\begin{schema}{Init\_PrioData}
  PrioData'
\where
  priority' = (\lambda  x: TASK @ 0)
\end{schema}

\begin{theorem}{PrioDataInit}
\exists  PrioData' @ Init\_PrioData
\end{theorem}

\begin{zproof}[PrioDataInit]
prove by reduce;
\end{zproof}

\begin{schema}{Task}
  TaskData\\
  StateData\\
  ContextData\\
  PrioData
\where
  tasks = TASK \setminus  (state \inv  \limg  \{nonexistent\} \rimg )\\
  state \inv  \limg  \{running\} \rimg  = \ran  running\_tasks\\
  \forall  pt: state \inv  \limg  \{ready\} \rimg ; r: \ran  running\_tasks | executable(pt) = executable(r) @ priority(r) \geq  priority(pt)
\end{schema}

\begin{zproof}[Task\$domainCheck]
invoke TaskData;
prove;
\end{zproof}

\begin{theorem}{targetInDomExe}
\forall  Task; target?: TASK | state(target?) \neq  nonexistent @ target? \in  \dom  executable \land  executable(target?) \in  cores
\end{theorem}

\begin{zproof}[targetInDomExe]
invoke Task;
invoke TaskData;
use applyInRanPfun[TASK, CORE][A := TASK, B := cores, f := executable, a := target?];
prove;
\end{zproof}

\begin{schema}{\Delta Task}
  Task\\
  Task'
\where
  \forall  st: TASK | state'(st) \neq  state(st) @ state(st) \mapsto  state'(st) \in  transition
\end{schema}

%\begin{schema}{Init} %uncomment this when animate with ProZ
%\begin{schema}{Init\_Task} %uncomment this when prove with Z/Eves
  Task'
\where
  Init\_TaskData\\
  Init\_StateData\\
  Init\_ContextData\\
  Init\_PrioData
\end{schema}

\begin{theorem}{TaskInit}
\forall  r: cores \inj  TASK; e: TASK \psurj  cores | r \neq  \emptyset \land  r = cores \cross  idles \land  e = r \inv  @ \exists  Task' @ Init\_Task
\end{theorem}

\begin{zproof}[TaskInit]
instantiate running\_tasks' == r, executable' == e;
prove by reduce;
apply extensionality to predicate idles = TASK \setminus  ((\{  x: TASK @ (x, nonexistent) \} \oplus  (idles \cross  \{running\})) \inv  \limg  \{nonexistent\} \rimg );
apply extensionality to predicate (\{  x: TASK @ (x, nonexistent) \} \oplus  (idles \cross  \{running\})) \inv  \limg  \{running\} \rimg  = idles;
with enabled (applyOverride) prove;
apply applyOverride to expression (\{  x: TASK @ (x, nonexistent) \} \oplus  (idles \cross  \{running\})) x\_\_0;
prove;
\end{zproof}

\begin{schema}{createTaskSpeCoreN\_T}
  \Delta Task\\
  target?: TASK\\
  newpri?: \nat \\
  executeCore: CORE
\where
  executeCore \in  cores\\
  state(target?) = nonexistent\\
  newpri? \leq  priority (running\_tasks(executeCore))\\
  tasks' = tasks \cup  \{target?\}\\
  running\_tasks' = running\_tasks\\
  executable' = executable \oplus  \{(target? \mapsto  executeCore)\}\\
  state' = state \oplus  \{(target? \mapsto  ready)\}\\
  \Xi ContextData\\
  priority' = priority \oplus  \{(target? \mapsto  newpri?)\}
\end{schema}

\begin{zproof}[createTaskSpeCoreN\_T\$domainCheck]
prove;
\end{zproof}

\begin{schema}{findACore\_T}
  Task\\
  target?: TASK\\
  newpri?: \nat \\
  executeCore?: CORE\\
  executeCore: CORE
\where
  executeCore? \notin  cores\\
  executeCore \in  cores\\
  \exists  tcs, cs: \finset  cores | tcs = \{  pc: cores | newpri? > priority (running\_tasks(pc)) \} @ (tcs = \emptyset \implies  cs = cores) \land  (tcs \neq  \emptyset \implies  cs = tcs) \land  (\forall  oc: cs @ (executeCore \in  cs \land  \# (executable \inv  \limg  \{executeCore\} \rimg ) \leq  \# (executable \inv  \limg  \{oc\} \rimg )))
\end{schema}

\begin{zproof}[findACore\_T\$domainCheck]
invoke Task;
invoke TaskData;
prove;
\end{zproof}

\begin{zed}
CreateTaskN\_T \defs ([executeCore?, executeCore: CORE | executeCore? \in  cores \land  executeCore = executeCore?] \lor  findACore\_T) \land  createTaskSpeCoreN\_T
\end{zed}

\begin{schema}{Reschedule}
  \Delta Task\\
  target?: TASK\\
  tasks?: \finset  TASK\\
  executable?: TASK \psurj  cores\\
  st?: STATE\\
  pri?: TASK \fun  \nat 
\where
  tasks' = tasks?\\
  target? \in  tasks?\\
  \dom  executable? = tasks?\\
  running\_tasks' = running\_tasks \oplus  \{(executable?(target?) \mapsto  target?)\}\\
  executable' = executable?\\
  state' = state \oplus  \{(target? \mapsto  running), (running\_tasks (executable?(target?)) \mapsto  st?)\}\\
  phys\_context' = phys\_context \oplus  \{(executable?(target?) \mapsto  log\_context(target?))\}\\
  log\_context' = log\_context \oplus  \{(running\_tasks (executable?(target?)) \mapsto  phys\_context (executable?(target?)))\}\\
  priority' = pri?
\end{schema}

\begin{zproof}[Reschedule\$domainCheck]
use applyInRanPfun[TASK, CORE][A := TASK, B := cores, f := executable?, a := target?];
prove;
\end{zproof}

\begin{zed}
disableReschedule \defs [Task | false] \land  Reschedule
\end{zed}

\begin{schema}{createTaskSpeCoreS\_T}
  \Delta Task\\
  target?: TASK\\
  newpri?: \nat \\
  executeCore: CORE
\where
  executeCore \in  cores\\
  state(target?) = nonexistent\\
  newpri? > priority (running\_tasks(executeCore))\\
  \exists  st?: STATE; tasks?: \finset  TASK; executable?: TASK \psurj  cores; pri?: TASK \fun  \nat  | st? = ready \land  tasks? = tasks \cup  \{target?\} \land  executable? = executable \oplus  \{(target? \mapsto  executeCore)\} \land  pri? = priority \oplus  \{(target? \mapsto  newpri?)\} @ Reschedule
\end{schema}

\begin{zproof}[createTaskSpeCoreS\_T\$domainCheck]
prove;
\end{zproof}

\begin{zed}
CreateTaskS\_T \defs ([executeCore?, executeCore: CORE | executeCore? \in  cores \land  executeCore = executeCore?] \lor  findACore\_T) \land  createTaskSpeCoreS\_T
\end{zed}

\begin{zed}
CreateTask\_T \defs CreateTaskN\_T \lor  CreateTaskS\_T
\end{zed}

\begin{schema}{DeleteTaskN\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in  tasks \setminus  idles\\
  state(target?) \in  \{ready, blocked, suspended\}\\
  tasks' = tasks \setminus  \{target?\}\\
  running\_tasks' = running\_tasks\\
  executable' = \{target?\} \ndres  executable\\
  state' = state \oplus  \{(target? \mapsto  nonexistent)\}\\
  phys\_context' = phys\_context\\
  log\_context' = log\_context \oplus  \{(target? \mapsto  bare\_context)\}\\
  \Xi PrioData\\
  topReady! = running\_tasks (executable(target?))
\end{schema}

\begin{zproof}[DeleteTaskN\_T\$domainCheck]
use targetInDomExe;
with normalization rewrite;
\end{zproof}

\begin{schema}{findTopReady}
  Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in  tasks\\
  state(topReady!) = ready\\
  executable(topReady!) = executable(target?)\\
  \forall  rt: state \inv  \limg  \{ready\} \rimg  | executable(rt) = executable(topReady!) @ priority(topReady!) \geq  priority(rt)
\end{schema}

\begin{zproof}[findTopReady\$domainCheck]
prove by reduce;
\end{zproof}

\begin{schema}{DeleteTaskS\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  target? \in  tasks \setminus  idles\\
  state(target?) = running\\
  findTopReady\\
  tasks' = tasks \setminus  \{target?\}\\
  running\_tasks' = running\_tasks \oplus  \{(executable(target?) \mapsto  topReady!)\}\\
  executable' = \{target?\} \ndres  executable\\
  state' = state \oplus  \{(topReady! \mapsto  running), (target? \mapsto  nonexistent)\}\\
  phys\_context' = phys\_context \oplus  \{(executable(target?) \mapsto  log\_context(topReady!))\}\\
  log\_context' = log\_context \oplus  \{(target? \mapsto  bare\_context)\}\\
  \Xi PrioData
\end{schema}

\begin{zproof}[DeleteTaskS\_T\$domainCheck]
use targetInDomExe;
prove;
\end{zproof}

\begin{zed}
DeleteTask\_T \defs DeleteTaskN\_T \lor  DeleteTaskS\_T
\end{zed}

\begin{schema}{ExecuteRunningTask\_T}
  \Delta Task\\
  target!: \finset  TASK
\where
  \Xi TaskData\\
  \Xi StateData\\
  \forall  c: cores @ phys\_context'(c) \neq  phys\_context(c)\\
  log\_context' = log\_context\\
  \Xi PrioData\\
  target! = \ran  running\_tasks
\end{schema}

\begin{zproof}[ExecuteRunningTask\_T\$domainCheck]
prove;
\end{zproof}

\begin{schema}{SuspendTaskN\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) \in  \{ready, blocked\}\\
  target? \notin  idles\\
  \Xi TaskData\\
  state' = state \oplus  \{(target? \mapsto  suspended)\}\\
  \Xi ContextData\\
  \Xi PrioData\\
  topReady! = running\_tasks (executable(target?))
\end{schema}

\begin{zproof}[SuspendTaskN\_T\$domainCheck]
use targetInDomExe;
prove;
split state(target?) = ready;
prove;
\end{zproof}

\begin{schema}{SuspendTaskS\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = running\\
  target? \notin  idles\\
  findTopReady\\
  \exists  st?: STATE | st? = suspended @ Reschedule[tasks/tasks?, executable/executable?, priority/pri?, topReady!/target?]
\end{schema}

\begin{schema}{SuspendTaskO\_T}
  \Xi Task\\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = suspended\\
  topReady! = running\_tasks (executable(target?))
\end{schema}

\begin{zproof}[SuspendTaskO\_T\$domainCheck]
use targetInDomExe;
prove;
\end{zproof}

\begin{zed}
SuspendTask\_T \defs SuspendTaskN\_T \lor  SuspendTaskS\_T \lor  SuspendTaskO\_T
\end{zed}

\begin{schema}{ResumeTaskN\_T}
  \Delta Task\\
  target?: TASK
\where
  state(target?) = suspended\\
  priority(target?) \leq  priority (running\_tasks (executable(target?)))\\
  \Xi TaskData\\
  state' = state \oplus  \{(target? \mapsto  ready)\}\\
  \Xi ContextData\\
  \Xi PrioData
\end{schema}

\begin{zproof}[ResumeTaskN\_T\$domainCheck]
use targetInDomExe;
prove;
\end{zproof}

\begin{schema}{ResumeTaskS\_T}
  \Delta Task\\
  target?: TASK
\where
  state(target?) = suspended\\
  priority(target?) > priority (running\_tasks (executable(target?)))\\
  \exists  st?: STATE | st? = ready @ Reschedule[tasks/tasks?, executable/executable?, priority/pri?]
\end{schema}

\begin{zproof}[ResumeTaskS\_T\$domainCheck]
use targetInDomExe;
prove;
\end{zproof}

\begin{zed}
ResumeTask\_T \defs ResumeTaskN\_T \lor  ResumeTaskS\_T
\end{zed}

\begin{schema}{ChangeTaskPriorityN\_T}
  \Delta Task\\
  newpri?: \nat \\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = ready \implies  newpri? \leq  priority (running\_tasks (executable(target?)))\\
  state(target?) = running \implies  (\forall  rt: state \inv  \limg  \{ready\} \rimg  | executable(rt) = executable(target?) @ newpri? \geq  priority(rt))\\
  state(target?) \neq  nonexistent\\
  target? \in  idles \implies  newpri? = 0\\
  \Xi TaskData\\
  \Xi StateData\\
  \Xi ContextData\\
  priority' = priority \oplus  \{(target? \mapsto  newpri?)\}\\
  topReady! = running\_tasks (executable(target?))
\end{schema}

\begin{zproof}[ChangeTaskPriorityN\_T\$domainCheck]
use targetInDomExe;
prove;
cases;
prove;
next;
use targetInDomExe[rt/target?];
prove;
next;
\end{zproof}

\begin{schema}{ChangeTaskPriorityS\_T}
  \Delta Task\\
  newpri?: \nat \\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = ready\\
  newpri? > priority (running\_tasks (executable(target?)))\\
  target? \in  idles \implies  newpri? = 0\\
  \exists  st?: STATE; pri?: TASK \fun  \nat  | st? = ready \land  pri? = priority \oplus  \{(target? \mapsto  newpri?)\} @ Reschedule[tasks/tasks?, executable/executable?]\\
  topReady! = target?
\end{schema}

\begin{zproof}[ChangeTaskPriorityS\_T\$domainCheck]
use targetInDomExe;
prove;
\end{zproof}

\begin{schema}{ChangeTaskPriorityD\_T}
  \Delta Task\\
  newpri?: \nat \\
  target?: TASK\\
  topReady!: TASK
\where
  state(target?) = running\\
  target? \in  idles \implies  newpri? = 0\\
  findTopReady\\
  newpri? < priority(topReady!)\\
  \exists  st?: STATE; pri?: TASK \fun  \nat  | st? = ready \land  pri? = priority \oplus  \{(target? \mapsto  newpri?)\} @ Reschedule[tasks/tasks?, executable/executable?, topReady!/target?]
\end{schema}

\begin{zed}
ChangeTaskPriority\_T \defs ChangeTaskPriorityN\_T \lor  ChangeTaskPriorityS\_T \lor  ChangeTaskPriorityD\_T
\end{zed}

\begin{schema}{MigrationN\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newCore?: cores
\where
  state(target?) \in  \{ready, blocked, suspended\}\\
  state(target?) = ready \implies  priority(target?) \leq  priority (running\_tasks(newCore?))\\
  target? \notin  idles\\
  newCore? \neq  executable(target?)\\
  tasks' = tasks\\
  running\_tasks' = running\_tasks\\
  executable' = executable \oplus  \{(target? \mapsto  newCore?)\}\\
  \Xi StateData\\
  \Xi ContextData\\
  \Xi PrioData\\
  topReady! = running\_tasks(newCore?)
\end{schema}

\begin{zproof}[MigrationN\_T\$domainCheck]
use targetInDomExe;
prove;
with normalization prove;
\end{zproof}

\begin{schema}{MigrationS\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newCore?: cores
\where
  state(target?) = ready\\
  priority(target?) > priority (running\_tasks(newCore?))\\
  target? \notin  idles\\
  newCore? \neq  executable(target?)\\
  \exists  st?: STATE; executable?: TASK \psurj  cores | st? = ready \land  executable? = executable \oplus  \{(target? \mapsto  newCore?)\} @ Reschedule[tasks/tasks?, priority/pri?]\\
  topReady! = target?
\end{schema}

\begin{zproof}[MigrationS\_T\$domainCheck]
use targetInDomExe;
prove;
\end{zproof}

\begin{schema}{MigrationRuN\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newCore?: cores
\where
  state(target?) = running\\
  priority(target?) \leq  priority (running\_tasks(newCore?))\\
  target? \notin  idles\\
  newCore? \neq  executable(target?)\\
  findTopReady\\
  \exists  st?: STATE; executable?: TASK \psurj  cores | st? = ready \land  executable? = executable \oplus  \{(target? \mapsto  newCore?)\} @ Reschedule[tasks/tasks?, priority/pri?, topReady!/target?]
\end{schema}

\begin{zproof}[MigrationRuN\_T\$domainCheck]
use targetInDomExe;
prove;
\end{zproof}

\begin{schema}{MigrationRuS\_T}
  \Delta Task\\
  target?: TASK\\
  topReady!: TASK\\
  newCore?: cores
\where
  state(target?)= running\\
  priority(target?) > priority (running\_tasks(newCore?))\\
  target? \notin  idles\\
  newCore? \neq  executable(target?)\\
  findTopReady\\
  tasks' = tasks\\
  running\_tasks' = running\_tasks \oplus  \{(executable(target?) \mapsto  topReady!), (newCore? \mapsto  target?)\}\\
  executable' = executable \oplus  \{(target? \mapsto  newCore?)\}\\
  state' = state \oplus  \{(topReady! \mapsto  running), (running\_tasks(newCore?) \mapsto  ready)\}\\
  phys\_context' = phys\_context \oplus  \{(executable(topReady!) \mapsto  log\_context(topReady!)), (newCore? \mapsto  phys\_context (executable(topReady!)))\}\\
  log\_context' = log\_context \oplus  \{(running\_tasks(newCore?) \mapsto  phys\_context(newCore?))\}\\
  priority' = priority
\end{schema}

\begin{zproof}[MigrationRuS\_T\$domainCheck]
prove;
cases;
use targetInDomExe;
prove;
next;
use targetInDomExe[topReady!/target?];
invoke findTopReady;
prove;
next;
\end{zproof}

\begin{zed}
Migration\_T \defs MigrationN\_T \lor  MigrationS\_T \lor  MigrationRuN\_T \lor  MigrationRuS\_T
\end{zed}

\begin{theorem}{createTaskOverTwoCores}
\forall  Task; target?, i1, i2: TASK; newpri?: \nat ; executeCore?, c1, c2: CORE | c1 \neq  c2 \land  cores = \{c1, c2\} \land  idles = \{i1, i2\} \land  running\_tasks = \{c1 \mapsto  i1, c2 \mapsto  i2\} \land  newpri? = 1 \land  tasks = \{i1, i2\} \land  executeCore? = c1 \land  executable = \{i1 \mapsto  c1, i2 \mapsto  c2\} \land  CreateTask\_T @ target? \in  tasks' \land  state' target? = running \land  priority' target? = 1 \land  executable' target? = c1
\end{theorem}

\begin{zproof}[createTaskOverTwoCores]
apply extensionality to predicate idles = \{i1\} \cup  \{i2\};
instantiate y == i1;
apply extensionality to predicate cores = \{c1\} \cup  \{c2\};
instantiate y == c1;
rewrite;
invoke Task;
invoke PrioData;
instantiate i == i1;
prove by reduce;
\end{zproof}

\begin{theorem}{createTaskOverSignalCore}
\forall  Task; target?, i1: TASK; newpri?: \nat ; executeCore?, c1: CORE | cores = \{c1\} \land  idles = \{i1\} \land  running\_tasks = \{c1 \mapsto  i1\} \land  executable = \{i1 \mapsto  c1\} \land  tasks = \{i1\} \land  executeCore? = c1 \land  newpri? = 1 \land  CreateTask\_T @ target? \in  tasks' \land  state' target? = running \land  priority' target? = 1 \land  executable' target? = c1
\end{theorem}

\begin{zproof}[createTaskOverSignalCore]
apply extensionality to predicate idles = \{i1\};
instantiate y == i1;
apply extensionality to predicate cores = \{c1\};
instantiate y == c1;
rewrite;
invoke Task;
invoke PrioData;
instantiate i == i1;
prove by reduce;
\end{zproof}


